Nuprl Definition : ma-single-pre1
0,22
postcript
pdf
ma-single-pre1(
x
;
A
;
a
;
T
;
y
,
v
.
P
(
y
;
v
))
== (with ds:
x
:
A
== (
action
a
:
T
== (
precondition
a
(v) is
== (
s
,
v
.
P
(
s
(
x
);
v
) s v)
latex
Definitions
(with ds:
ds
action
a
:
T
precondition
a
(v) is
P
s v)
,
x
:
v
,
x
,
y
.
t
(
x
;
y
)
,
f
(
a
)
FDL editor aliases
ma-single-pre1
origin
s,v. P(s(x);v) s v) s,v. P(s(x);v) s v) x,y. t(x;y)